OP
←(V1,A1)
NIL
NIL
NIL
ISVAR(V1);;
C(V1,A1);;

ITERATIVE
TGCD
NIL
NIL
NIL
NEWVAR(Y1);>(X,(0)); >(Y,(0));C(X1,X);C(Y1,Y);;
C(X1,V1);C(Y1,V2);VGC(V1 V2 V3);VGC(X,Y,V3);;
C(X1,E1);C(Y1,E2); VGC(V1,V2,V4);VGC(E1,E2,V4);>((PLUS V1 V2),(PLUS E1 E2));;
NIL
CGC(X,Y X1);;
CGC(X,Y,X1);;

AXIOM
REDUCE
NIL
NIL
NIL
 =(X(PLUS V1 V2)); =(Y(PLUS E1 E2));=(E2 V2); =(E1,(DIFFERENCE V1 W));>(W (0));;
>(X,Y);;


AXIOM
TGCD1
NIL
NIL
NIL
VGC((DIFFERENCE B C) C A));;
VGC(B,C,A);;

AXIOM
TGCD2
NIL
NIL
NIL
VGC(B,C,A);;
VGC(C B A);;

NIL
NIL

ISVAR(M1);>(M,(0)); >(N,(0));VGC(M N GCDMN);;

T

((C T NIL NIL (X,*))
(> NIL NIL NIL NIL)
(= T NIL NIL NIL) 
(VGC T NIL NIL NIL) 
(CGC T NIL NIL NIL) 
               )

T
((ADD1(X)(/( X/+ 1 /) ))
 (SUB1(X)(/( X/- 1 /) ))
 (PLUS(X Y)( /(X /+ Y/)) ) )